k:FinProbSpace, n:, X, Y:RandomVariable(k;n). X + Y  RandomVariable(k;n) 

latex

Definitions	t  T, , x:A. B(x), ||as||, P & Q, i  j < k, a < b, P  Q, False, A, A  B, , {x:A| B(x)} , {i..j}, #$n, Void, x:AB(x), l[i], x. t(x), a  j < b. E(j), s = t, type List, , Type, f(a), r + s, x.A(x), X + Y, RandomVariable(p;n), FinProbSpace
Lemmas	qadd wf, nat wf, qsum wf, select wf, int seg wf, int inc rationals, length wf1, rationals wf